A:Type, l:IdLnk, tg:Id, I:MaInterface(A).
((tg  ma-interface-tags(I)))
 Normal(A,I)
 (source(l)  ma-interface-locs(I))
 R-Feasible(triggersGlue(A; l; tg; ma-interface-ds(I;source(l)); (I(source(l)).2))) 

latex

Definitions

x:A. B(x), P  Q, P  Q, P  Q, , T, True, t  T, x. t(x), P & Q, a:A fp B(a), Knd, Top, t.2, A c B, S  T, ma-interface-conds(I;i), t.1, f(x), A, SQType(T), {T}, (x  l), b, x:A. B(x), A  B, False, tt, if b then t else f fi , x(s), MaInterface(T), ma-interface-locs(I), Normal(A,I), x  dom(f), fpf-domain(f), Normal(T), Normal(ds), , ma-interface-domb(I;i;k)

Lemmas

R-Feasible wf, squash wf, true wf, es realizer wf, triggersGlue wf, Knd wf, assert wf, fpf-dom wf, Kind-deq wf, fpf-trivial-subtype-top, decl-state wf, top wf, hasloc wf, lsrc wf, fpf wf, Id wf, ma-interface-ds wf, ma-interface-conds-equals, l member wf, ma-interface-locs wf, ma-interface-normal wf, not wf, ma-interface-tags wf, ma-interface wf, IdLnk wf, assert-ma-interface-domb, ma-interface-dom-hasloc, fpf-ap wf, member-fpf-domain, id-deq wf, subtype rel product, subtype rel list, subtype rel set, subtype rel function, subtype-set-hasloc, triggersGlue feasible, ma-interface-conds wf, fpf-domain wf, assert-deq-member, ma-interface-dom wf, rcv wf, Knd sq, ma-interface-tags-property2, nat wf, length wf1, select wf, isrcv wf